T:Type, as,bs:(T List). iseg(T; as; bs)  iseg(T; bs; as)  (as = bs) 

latex

Definitions	guard(T), P  Q, iseg(T; l1; l2), b, null(as), prop{i:l}, False, P  Q, P  Q, x:A. B(x), P  Q, t  T
Lemmas	cons iseg, null wf, assert wf, iseg wf, iseg nil, implies functionality wrt iff